/* Assignment 1 */
/* Assume that there are two readers and the counter has 3 bits */

#define READERS 0
#define COUNTER_SIZE 4
#define MAX 1 
bit counter[COUNTER_SIZE * 2] = 0;

inline convert_to_int() {
    int value = 0;
    d_step {
        for (i : (COUNTER_SIZE - 1) .. 0) {
            value = value * 2;
            value = value + lcounter[i];
        }
    };
    printf("MSC: %d\n", value);
    assert(value >= 0 && value < 5);
}

inline increment() {
        int current_bit = 0;
        lcounter[current_bit + COUNTER_SIZE]++;
        lcounter[COUNTER_SIZE - 1 - current_bit] = lcounter[current_bit + COUNTER_SIZE];
        do :: true ->  
            if :: (current_bit < COUNTER_SIZE) && (lcounter[current_bit + COUNTER_SIZE] == 0) ->
                current_bit++;
                lcounter[current_bit + COUNTER_SIZE]++;
                lcounter[COUNTER_SIZE - 1 - current_bit] = lcounter[current_bit + COUNTER_SIZE];
               :: else -> break;
            fi;
        od;
        convert_to_int();
}

inline write_local_to_global() {
    for (i : 0 .. (COUNTER_SIZE * 2 - 1)) {
        counter[i] = lcounter[i];
    }
}

active proctype writer() {
    bit lcounter[COUNTER_SIZE * 2] = 0;
    int i;
    do :: increment();
update:     write_local_to_global();
    od        
}

inline read_from_global_to_local() {
    for (i : (COUNTER_SIZE * 2 - 1) .. 0) {
        buffer[i] = counter[i];
    }
}



/*active[READERS] proctype reader() {
    bit buffer[COUNTER_SIZE * 2] = 0;
    bit lcounter[COUNTER_SIZE] = 0;
    int i;
    bool max;
    do :: true;
        read_from_global_to_local();
        max = false;
        for (i : 0 .. (COUNTER_SIZE - 1)) {
            if 
                :: (max == true) -> lcounter[COUNTER_SIZE - 1 - i] = MAX;
                :: else -> lcounter[COUNTER_SIZE - 1 - i] = buffer[i]; 
            fi;
            max = (buffer[i] != buffer[(COUNTER_SIZE * 2) - i - 1]);
        }
    od
}*/

ltl aud_writer { []writer@update -> <>writer@inc }
